import Mathlib.Data.Real.Basic
import Mathlib.Tactic

namespace CNVS

/--
Convergenza locale quantitativa.

`ConvAt D Obs ε` è vera se la distanza assoluta
tra dato dichiarato e dato osservato è entro la tolleranza ε.
-/
def ConvAt (D Obs ε : ℝ) : Prop :=
  |D - Obs| ≤ ε

/--
Verifica locale quantitativa.

La verifica locale passa se:
1. la tupla è formalmente ammissibile;
2. il dato dichiarato converge con il dato osservato.
-/
def VLocalQuantitative
    (Form : Prop)
    (D Obs ε : ℝ) : Prop :=
  Form ∧ ConvAt D Obs ε

/--
Test 1:
Se il dato osservato coincide esattamente col dato dichiarato
e la tolleranza è non negativa, allora la convergenza locale passa.
-/
theorem exact_observation_converges
    (D ε : ℝ)
    (hε : 0 ≤ ε) :
    ConvAt D D ε := by
  unfold ConvAt
  simpa using hε

/--
Test 2:
Se la verifica locale quantitativa passa,
allora la convergenza `ConvAt` è effettivamente vera.
Non è tautologico: estrae il secondo componente della verifica locale.
-/
theorem local_verification_implies_convergence
    (Form : Prop)
    (D Obs ε : ℝ) :
    VLocalQuantitative Form D Obs ε →
    ConvAt D Obs ε := by
  intro h
  exact h.2

/--
Test 3:
Se la verifica locale quantitativa passa,
allora anche la forma strutturale è valida.
-/
theorem local_verification_implies_formal_admissibility
    (Form : Prop)
    (D Obs ε : ℝ) :
    VLocalQuantitative Form D Obs ε →
    Form := by
  intro h
  exact h.1

/--
Test 4:
Se la forma è valida e la differenza è entro ε,
allora la verifica locale quantitativa passa.
-/
theorem convergence_and_form_imply_local_verification
    (Form : Prop)
    (D Obs ε : ℝ)
    (hForm : Form)
    (hConv : |D - Obs| ≤ ε) :
    VLocalQuantitative Form D Obs ε := by
  exact ⟨hForm, hConv⟩

/--
Esempio concreto:
D = 10, Obs = 10.1, ε = 0.2.
Lean verifica che la convergenza passa.
-/
example :
    ConvAt 10 10.1 0.2 := by
  norm_num [ConvAt]

/--
Esempio concreto negativo:
D = 10, Obs = 11, ε = 0.2.
Lean verifica che la convergenza NON passa.
-/
example :
    ¬ ConvAt 10 11 0.2 := by
  norm_num [ConvAt]

end CNVS